T, T':Type{i}, L:(T List), f:({x:T| (x  L)} T'), P:(T'T'{i'}).
(x, y:T. (x  L)  (y  L)  P(f(x),f(y)))  (x,ymapl(f;L).  P(x,y)) 

latex

Definitions	x:A. B(x), , P  Q, x(s1,s2), mapl(f;l), map(f;as), Y, True, Top, x,y. t(x;y), t  T, P & Q, P  Q, {T}, l[i], {i..j}, ||as||, i  j < k, hd(l), nth_tl(n;as), if b then t else f fi , i z j, b, i <z j, tt, ff, xL. P(x), x:A. B(x), A c B, P  Q, P  Q, (x  l)
Lemmas	pairwise-nil, l member wf, pairwise-cons, cons member, select member, length wf1, non neg length, mapl wf, le wf